CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THEOREM];

EDIT-STRATEGY-IS: 
DEPTH[2]∨LENGTH[2];

ELAPSED-TIME =3117

NIL 1 2
1 ¬(P(z,x)∧P(x,y));3 4
2 P(G22(x),x);G2
3 ¬G(x,y);THEOREM
4 P(x,z)∧P(z,y)⊃G(x,y);G1